ML[2]

Meta Language

R. Milner et al, 1973

A strict higher-order functional language with statically-checked polymorphic types, garbage collection and a formal semantics. It started out as the metalanguage for the Edinburgh LCF proof assistant. (LCF="Logic for Computable Functions") See SML[1].

LCF ML

The original ML, implemented in Stanford LISP.

"A Metalanguage for Interactive Proof in LCF", M. J. C. Gordon et al, Conference Record of the 5th Annual ACM Symposium on Principles of Programming Languages, ACM 1978.